COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR t1 t2 t3 t4 ε tower
C00004 ENDMK
C⊗;
declare INDVAR t1 t2 t3 t4 ε tower;
declare INDVAR s s0 s1 s2 s3 ε situation;

declare PREDCONST movable(tower,tower,situation),on(tower,tower,situation);
declare PREDCONST reachable(situation,situation);
declare OPCONST move(tower,tower,situation) = situation;
declare PREDPAR P 1;

axiom move:
	∀t1 t2 s.(movable(t1,t2,s) ⊃ on(t1,t2,move(t1,t2,s))
		∧ ∀t3 t4.(¬(t3=t1) ⊃ (on(t3,t4,move(t1,t2,s)) ≡ on(t3,t4,s))))
	∀t1 t2 s.(¬movable(t1,t2,s) ⊃ move(t1,t2,s) = s)
;;

axiom reachable:
	∀t1 t2 s.(movable(t1,t2,s) ⊃ reachable(s,move(t1,t2,s)))
	∀s.reachable(s,s)
	∀s1 s2 s3.(reachable(s1,s2) ∧ reachable(s2,s3) ⊃ reachable(s1,s3))
	∀s1 s2 t1 t2.(reachable(s1,s2) ∧movable(t1,t2,s2) ⊃
				reachable(s1,move(t1,t2,s2)))
	∀s0.(P(s0) ∧ ∀s t1 t2.(P(s) ∧ movable(t1,t2,s) ⊃ P(move(t1,t2,s)))
				⊃ ∀s.(reachable(s0,s) ⊃ P(s)))
;;